Nuprl Lemma : FIFO_wf
11,40
postcript
pdf
es
:ES{i}. FIFO{i:l}(
es
)
Type{i'}
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
FIFO
,
Lemmas
es-E
wf
,
es-state
wf
,
es-loc
wf
,
fifo
wf
,
event
system
wf
origin
es:ES{i}. FIFO{i:l}(es) 
Type{i'} es:ES{i}. FIFO{i:l}(es) Type{i'} x:A. B(x) T